structure Main : MAIN =
struct

  
  structure Ast = Ast()
  structure Types = Types()
  structure Types2 = Types2 ()
  structure Ir = Ir (structure Types = Types)
  structure Asm = Assem()
   
  structure C = CodeGenMain (structure Ir = Ir
                             structure Assem = Asm)
  structure Temp = Temp
  structure E = ErrorMsg
  structure E2 = AsmErrorMsg
  
  structure AsmProver = AsmProver (structure Asm = Asm)

  structure Parse = Parse (structure Ast = Ast) 
  structure Ppast = Ppast (structure Ast = Ast)

  structure T = TypeCheck (structure Ast = Ast
                           structure Types = Types2)
  structure A = Ast2Ir (structure Ast = Ast
                        structure Ir = Ir
                        structure Types = Types)
  structure OptOnAst = OptOnAst (structure Ast = Ast)  
  structure VcGenMain = VcGenMain (structure Ir = Ir)
  
  structure X86Asm = X86Assem ()
  structure X86Parse = X86Parse (structure Asm = X86Asm)
  structure X86Main = X86Main (structure Assem = Asm
                               structure X86Assem = X86Asm)
  
  exception ParseFailed
  exception TypeCheckFailed
  exception OptAstFailed
  exception Ast2IrFailed
  exception SrcPtrLogicFailed
  exception EmitAssemFailed
  exception AsmPtrLogicFailed
  exception EmitProofFailed
  exception ExeFailed
  exception Success
  
  exception CompilationFail
  
  datatype fileSort
    = C
    | S
    | Other
  
  fun fileSort s =
      case List.rev (String.explode s)
       of (#"c") :: (#".") :: _ => C
        | (#"C") :: (#".") :: _ => C
        | (#"s") :: (#".") :: _ => S
        | (#"S") :: (#".") :: _ => S
        | _ => Other
       
  fun main filename =
      let val _ = (E.reset();
                   E2.reset();
                   Temp.reset();
                   E.fileName := filename;
                   E2.fileName := filename(*;
                   Compiler.Control.Print.printDepth := 100;
                   Compiler.Control.Print.printLength := 100*))
          fun say s = if (!Control.doShowPass) then print s else ()
      in  case fileSort filename
           of C => let val _ = say ("compile: "^filename^" starting\n")
              val _ = say "lexing and parsing starting\n"           
              val iniAst = Parse.parse filename
              val _ = if (!E.anyErrors) then raise ParseFailed else ()
              val _ = say "lexing and parsing finished\n\n"

              val _ = if (!Control.doOutputAst)
                      then let val _ = say "output the initial AST starting\n"
                               val out1 = TextIO.openOut(filename^".ast1..c")
			       val s1 = Ppast.top iniAst
			       val _ = TextIO.output(out1, s1)
			       val _ = TextIO.closeOut out1
                           in  say "output the initial AST finished\n"
                           end
                      else ()                
                         
              val _ = say "type check starting\n"
              val _ = T.typeCkProg iniAst 
              val _ = if (!E.anyErrors) then raise TypeCheckFailed else ()
              val _ = say "type check finished\n\n"
                           
              val ast = if (!(Control.doOptOnAst))
                        then (say "optimize the AST starting\n"			    
			    ; say "optimize the AST finished\n\n"
			    ; OptOnAst.top iniAst)
                        else (say "the initial AST\n";
                             iniAst)

	      val _ = if (!Control.doOptOnAst) andalso (!Control.doOutputOptAst)
		      then let val _ = say "output the optimized AST starting\n"
			       val out2 = TextIO.openOut(filename^".ast2..c")
			       val s2 = Ppast.top ast
			       val _ = TextIO.output(out2, s2)
			       val _ = TextIO.closeOut out2
			       val _ = if (!E.anyErrors) then raise OptAstFailed else ()
			       val _ = say "output the optimized AST finished\n\n"
			   in  ()
			   end
		      else ()          
              
              val _ = say "translate to IR starting\n"
              val ir = A.ast2ir ast 
              val _ = if (!E.anyErrors) then raise Ast2IrFailed else ()
              val _ = say "translate to IR finished\n\n"
             
              val _ = say "pointer logic based verification starting\n"
              val _ = VcGenMain.top ir
              val _ = if (!E.anyErrors) then raise SrcPtrLogicFailed else ()
              val _ = say "pointer logic based verification finished\n\n"             
              
              val _ = say "output x86 assembly starting\n"           
              val _ = C.ir2code ir
              val _ = if (!E.anyErrors) then raise EmitAssemFailed else ()
              val _ = say "output x86 assembly finished\n\n"              
(*
              val _ = say "assembly proof check starting\n"
              val _ = AsmProver.top(C.ir2pprf ir) handle AsmProverFail => (E.anyErrors := true)
              val _ = if (!E.anyErrors) then raise AsmPtrLogicFailed else ()
              val _ = say "assembly proof check finished\n\n"

              val _ = if (!Control.doCoq)
                      then let val _ = say "output coq proof starting\n"
                               val rtimer = Timer.startRealTimer ();
                               val _ = C.ir2prf ir
                               val _ = if (!E.anyErrors) then raise EmitProofFailed else ()
                               val _ = say "time consume : "
                               val _ = say (Time.toString (Timer.checkRealTimer rtimer))
                               val _ = say "s\n"
                               val _ = say "output coq proof finished\n\n"
                           in  ()
                           end
                      else ()
  *)    
              val _ = if (!Control.doKeepAssembly)
		      then () 
		      else let val _ = say "produce executables starting\n"
			       val _ = if (!Control.doSetFileName)
				       then OS.Process.system (String.concat ["gcc ",
                                                                              filename,
                                                                              ".s",
                                                                              " tcclib.o -o ",
                                                                              !Control.fileName])
				       else OS.Process.system (String.concat ["gcc ",
                                                                              filename,
                                                                              ".s",
                                                                              " tcclib.o -o ",
                                                                              filename,
                                                                              ".exe"])
			       val _ = if (!E.anyErrors) then raise  ExeFailed else ()
			       val _ = say "produce executables finished\n\n"
			   in  ()
			   end             
              
              val _ = if (!Control.doKeepAssembly)
                      then ()
                      else ignore (OS.Process.system ("rm "^filename^".s"))
              
              val _ = say ("compile: "^filename^" finished\n")
          in  ()
          end
        | S => let val _ = say ("compile: "^filename^" starting\n")
              val _ = say "lexing and parsing starting\n"           
              val iniAst = (X86Parse.parse filename) handle X86ParseFailed => raise ParseFailed
              val _ = if (!E2.anyErrors) then raise ParseFailed else ()
              val _ = say "lexing and parsing finished\n\n"
              
              val assem = X86Main.main iniAst

              val _ = say "assembly proof check starting\n"
              val _ = (AsmProver.top assem) handle AsmProverFail => (E2.anyErrors := true)
              val _ = if (!E2.anyErrors) then raise AsmPtrLogicFailed else ()
              val _ = say "assembly proof check finished\n\n"
              
              val _ = say "rebuild code heap for Coq starting\n"
	      val _ = C.rebdChs assem filename
	      val _ = say "rebuild code heap for Coq finished\n\n"

             
              val _ = say ("compile: "^filename^" finished\n")
          in  ()
          end
        | Other => raise Fail "compiler bug\n"
      end            
end
